\begin{tabbing}
$\forall$\=$a$:Id, $T$:Type, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, $P$:Top, $k$:Knd, $l$:IdLnk, $d_{1}$:$x$:Id fp$\rightarrow$ Type,\+
\\[0ex]${\it da}$:$a$:Knd fp$\rightarrow$ Type, $f$:(Id$\times$Top) List.
\-\\[0ex]${\it ds}$ $\parallel$ $d_{1}$
\\[0ex]$\Rightarrow$ locl($a$) : $T$ $\parallel$ ${\it da}$
\\[0ex]$\Rightarrow$ (\=with declarations \+
\\[0ex]ds:$d_{1}$
\\[0ex]da:${\it da}$
\\[0ex]$k$(v) sends $f$ s v on link $l$
\\[0ex]$\Vert\!+$ (\=with ds: ${\it ds}$\+
\\[0ex]action $a$:$T$
\\[0ex]precondition $a$(v) is
\\[0ex]$P$ s v))
\-\-
\end{tabbing}